TelescopingLet1.agda:6,10-11
Not in scope:
  ★
  at TelescopingLet1.agda:6,10-11
when scope checking ★
